\chapter{数据平面验证中的需求快速验证问题研究}
\label{cha:verify}
本章主要对数据平面中的需求快速验证问题进行研究。

\section{数据平面验证中的快速需求验证问题概述}
由于数据平面FIB收集需要一定时间，但是验证系统往往不能保证及时收到数据平面的全部更新信息，导致验证系统需要很长时间才能收集到网络中全部的FIB更新，我们将该问题称为“长尾到达”问题(Long-tail arrival)。有多种原因会导致上述情况发生，如：
\begin{enumerate}
  \item 网络设备路由软件失败
  \item 资源争用导致FIB计算缓慢
  \item 不稳定链路导致FIB计算阻尼
  \item Incast conjestion导致数据包丢失
\end{enumerate}

\subsection{数据平面验证中的长尾问题定义}

为了解决上述长尾到达问题，我们需要能够在未获取到所有设备更新的情况下能够提前知道最终验证结果。同时，也需要相应的增量式验证算法来实现数据平面增量式验证。

我们首先定义一致的提前检测。令 $M_K$ 表示经过了 $K$ 次更新的数据平面模型，$M_k$ 表示仅经过了 $k < K$ 次更新的数据平面模型。令 $ver$ 为需求检测函数，该函数以网络需求 $req$ 和模型 $M_k$ 为输入。由于 $M_k$ 只有部分信息网络数据平面信息，所以 $ver(req, M_k)$ 可能给出具体结果（即满足/不满足）或未知结果。

\begin{definition}
\textbf{数据平面提前验证}。对于一个网络需求 $req$，对任意一个数据平面模型 $M$ 和 $K$ 个 $M$ 上的更新，如果 $\exists k \le K$, $ver(req, M_k)$ 能够给出具体结果，而且 $ver(req, M_k) = ver(req, M_{k+1}) = ... = ver(req, M_K)$，则 $ver$ 实现了对 $req$ 的一致性提前检测。
\end{definition}



\section{相关工作}
近年来，研究人员已经提出了许多解决数据平面快速需求验证问题的方法。其中，增量式验证是一种有效的解决方案。增量式验证基于数据平面的增量更新，通过快速验证一部分FIB更新来降低验证时间，并且能够保证验证结果的正确性。以下是一些与增量式验证相关的工作：

\begin{enumerate}
\item \textbf{Delta-encoding}：一种用于减少网络验证负担的技术，通过利用相邻FIB更新之间的差异来压缩FIB更新，从而降低验证时间。
\item \textbf{Differential Verification}：一种基于差分验证的增量式验证方法，通过记录FIB更新前后的状态来识别出新旧FIB之间的差异，从而验证新FIB的正确性。
\item \textbf{Flexible Incremental Verification}：一种增量式验证框架，支持在保证验证结果正确性的同时，根据可用时间和系统资源动态调整验证深度，从而有效地降低验证时间。
\end{enumerate}

这些方法为数据平面增量式验证提供了有效的解决方案，但是还有许多需要进一步探索和研究的问题，如增量式验证的可扩展性和适用性，以及如何在不牺牲验证结果正确性的情况下进一步提高验证效率等。

\section{基于一致性数据平面模型的增量式提前验证设计}
\subsection{数据平面提前验证}
我们首先定义一致的提前检测。令$M_K$表示经过了$K$次更新的数据平面模型，$M_k$表示仅经过了$k < K$次更新的数据平面模型。令$ver$为需求检测函数，该函数以网络需求$req$和模型$M_k$为输入。由于$M_k$只有部分信息网络数据平面信息，所以$ver(req, M_k)$可能给出具体结果（即满足/不满足）或未知结果。

\begin{definition}
  一致性提前检测。对于一个网络需求$req$，对任意一个数据平面模型$M$和$K$个$M$上的更新，如果$\exists k \le K$, $ver(req, M_k)$能够给出具体结果，而且$ver(req, M_k) = ver(req, M_{k+1}) = ... = ver(req, M_K)$, 则$ver$实现了对$req$的一致性提前检测。
\end{definition}

\begin{theorem}
  基于\textbf{部分}一致性数据平面模型上的提前检查实现了一致性提前检测。
\end{theorem}

Formally, given a consistent inverse model $M_k$. For a loop detection requirement $req_l$, let $\var{ver}_l$ denote the verification function that checking loops using the hyper abstraction in \ref{sec:all-pair}, when $\var{ver}_l(M_k, req_l)$ gives concrete result, $\var{ver}_l$ achieves consistent early detection.
\begin{proof}
    If $\var{ver}_l$ does not achieve consistent early detection, then according to~\ref{def:ced}, $\exists k' > k: \var{ver}_l(M_k, req_l) \neq \var{ver}_l(M_{k'}, req_l)$. That means the loop check result is changed after applies $k'$ updates. Since $\var{ver}_l$ only checks loops among synchronized nodes, the only way to break a loop is to update the FIB of the synchronized nodes, however, $M_k$ is a consistent model that guarantees no updates on synchronized nodes, thus such $k'$ doesn't exist.
\end{proof}

\subsection{增量式数据平面提前验证}
我们首先说明 如何对常规需求执行一致的提前检测，包括路由、最短路径、任播和组播等。具体而言， 利用自动机理论 \cite{lewis1998elements}，将该问题转化为基于递减的验证图上的增量可达性查询问题 \cite{hanauer2020fully}。

\paragraph{验证图和一致部分验证}
对于每个数据包空间 $H$ 和源节点集合 $srcs$，系统 计算网络自动机和需求表达式自动机的交叉积自动机 $G_p$ 作为验证图 \cite{lewis1998elements, soule2014merlin, beckett2016don, hsu2020contra}。初始验证图包含满足以下两个条件的 $G$ 中的所有路径：

\begin{enumerate}
\item 从 $srcs$ 开始
\item 匹配所有正则表达式
\end{enumerate}

考虑图 \ref{fig:early-network} 中的网络和需求。要求子空间 $h$ 中进入 $S$ 的数据包必须沿着穿过 $W$ 和 $Y$ 中的一个节点的简单路径到达 $D$。图 \ref{fig:cmc-example}(b) 显示了具有初始状态 $S1$ 和接受状态 $D1$ 的验证图。

有了这个图，验证需求表达式等价于在验证图中找到能够到达接受状态的路径。具体而言，如果存在一条只由同步节点组成的路径，则需求表达式一致地得到满足。如果存在一条只由同步节点到达拒绝状态的路径，则需求表达式一致地不满足。否则，验证结果为“未知”。

\paragraph{递减更新和可达性查询}
随着更多节点被同步，网络中符合该时期要求的可能路径集合单调递减。考虑图 \ref{fig:early-network} 中的示例，在收到“更新 1”之后，如图 \ref{fig:cmc-example}(b) 所示，验证图仅包含绿色区域中的节点和边。在进一步收到“更新 2”后，$G_P$ 中不存在有效路径，这意味着无论如何通过其他设备转发 $h$，都无法满足图 \ref{fig:early-network} 中的需求。在这样的递减图中（即，边始终被删除，但从不被添加），可达性查询具有恒定的时间复杂度 \cite{hanauer2020fully}。

\begin{figure}
  \centering\includegraphics[width=0.8\linewidth]{figures/ced-example-new.pdf}\\[-.5em]
  % \vspace{-1em}
	\caption{数据平面需求示例}
  \label{fig:early-network}
\end{figure}

\begin{figure}[ht]
  \center
  \includegraphics[width=\textwidth]{ced-example-revise.pdf}
  \caption{满足一致性的提前检测例子}
  \label{fig:cmc-example}
\end{figure}

\begin{algorithm}[t]
  \caption{Fast Consistent Partial Verification for Regular-expression Requirements.}
  \label{alg:early-reg}
  \footnotesize
  \SetAlgoLined
  \SetKwInOut{Input}{Input}
  \SetKwInOut{Output}{Output}
  \SetKwProg{Fn}{Function}{:}{}
  \SetKw{Abort}{abort}
  \SetKw{Not}{~not~}

  \textbf{Initialization}: $\var{ecTable} = \{H \mapsto
  \var{CreateProductGraph}{G, \var{rexpr}, \var{Port}_{\var{in}}}\}$\;
  \Fn{$\var{ConsistentPartialVerification}{\var{ctx}}$}{
    $\var{EC} \gets \var{GetEC}{\var{ctx}.M}$\;
    $\Delta \var{sync} \gets \var{ctx}.\var{sync} \setminus \var{sync}$\;
    $\var{sync} \gets \var{ctx}.\var{sync}$,
    $D \gets \emptyset$\;
    \ForEach{$\var{ec} \in \{\var{ec} \in \var{EC} \mid \var{ec} \cap H \neq \emptyset\}$}{
      \If{$\var{ec} \notin \var{ecTable}$}{
        $(\var{ec}^\prime, G_P^\prime) \gets \var{FindEntryToSplit}{\var{ecTable}}$\;
        $\var{ecTable}[\var{ec}] \gets G_P$\;
        $D \gets D \cup \{\var{ec}^\prime\}$\;
      }
      $G_P\gets \var{ecTable}[\var{ec}]$\;
      \ForEach{$v \in \Delta\var{sync}$}{
        $G_P \gets \var{PruneIncompatibleEdges}{G_P, \var{ec}, v}$\;
      }
      $\var{ecTable}[\var{ec}] \gets G_P$\;
      \If{\Not $\var{Reachable}{\var{ec}, G_P}$}{
        \Return \emph{Unsatisfied}
      }
    }
    \ForEach{$\var{ec}^\prime \in D$}{
      $\var{Delete}{\var{ecTable}[\var{ec}^\prime]}$\;
    }
    \Return \emph{UNKNOWN}
  }
\end{algorithm}

\begin{algorithm}[t]
  \caption{Fast Consistent Partial Loop Detection}
  \label{alg:cpld}
  \footnotesize
  \DontPrintSemicolon
  \SetKwInOut{Input}{Input}
  \SetKwInOut{Output}{Output}
  \SetKwProg{Fn}{Function}{}{}
  \SetKw{Continue}{continue}
  \SetKw{Abort}{abort}
  \SetKw{True}{~true~}
  \SetKw{False}{~false~}
  \SetKw{And}{~and~}
  \Fn{$\var{ConsistentPartialLoopDetect}{\var{ctx}}$}{
    $G_{\var{hyper}} \gets \var{BuildHyperGraph}{G, \var{ctx}.\var{sync}}$\;
    $\Delta \var{sync} \gets \var{ctx}.\var{sync} \setminus \var{sync}$\;
    $\var{sync} \gets \var{ctx}.\var{sync}$,
    $\var{potentialResults} \gets \emptyset$\;
    \For{$v \in \Delta\var{sync}$}{
      $\var{results} \gets \var{DetectLoop}{v, \{\var{ec} \in \var{ctx}.M\},
        \emptyset, \text{\textbf{false}}}$\;
      \If{a deterministic loop is found}{
        \Return $\{\var{Loop}\}$\;
      }
      $\var{potentialResults} \gets \var{potentialResults} \cup \var{results}$\;
    }
    \Return $\var{potentialResults}$\;
  }
  \Fn{\var{DetectLoop}{$v,\var{EC},\var{path},\var{hyper}$}}{
    \If{$\var{EC} = \emptyset$}{
      \Return $\emptyset$\;
    }
    $\var{potentialResults} \gets \emptyset$\;
    \If{$v$ is external}{
      \Return $\{\var{NoLoop}\}$
    }\ElseIf{$v.\var{is\_hyper}$\And$v.\var{is\_biconnected}$}{
      $\var{potentialResults} \gets \var{potentialResults} \cup \{\var{Loop}\}$\;
    }\ElseIf{$v \in \var{path}$\And$\var{hyper} = \True$}{
      \Return $\{\var{Loop}\}$\;
    }\ElseIf{$v \in \var{path}$\And$\var{hyper} = \False$}{
      \Abort \emph{Loop}
    }
    \ForEach{$(v, u) \in G_{\var{hyper}}$}{
      $\var{validEC} \gets \var{EC} \cap \var{EC}(v, u)$,
      $\var{path}^\prime \gets \var{path} \cup \{v\}$\;
      $r \gets \var{DetectLoop}{u, \var{validEC},
        \var{path}^\prime, \var{hyper}\vee{u.\var{hyper}}}$\;
      $\var{potentialResults} \gets \var{potentialResults} \cup r$\;
    }
    \Return $\var{potentialResults}$\;
  }
\end{algorithm}

\section{实验结果}
我们展示了使用递减验证图方法对基于正则表达式的需求执行一致早期检测的效率。具体来说，我们使用LNet apsp子空间设置并检查所有对ToR到ToR的可达性。Flash总共生成5376个验证图，每个子空间验证器生成48个验证图。每个交换机的规则插入都打包为一个批。我们在处理每个批次后验证可达性，并使用（1）递减图查询（DGQ）方法和（2）模型遍历（MT，即使用深度优先遍历从每个源ToR遍历模型）来测量单个子空间验证器的验证执行时间。

图~\ref{fig:eval-cdf-auto-allpair}显示了验证时间的CDF。我们可以看到，DGQ（蓝色）比MT（橙色）更靠近y轴。DGQ和MT的中位数、平均值、99\%和最长时间分别为0.58/0.84/4.74/19.57ms和772.98/1522.22/5513.76/7466.87ms。与MT相比，Flash将99\%的执行时间提高了~1163x（4.74ms vs.s.5513.76ms）。因此，我们可以得出结论，递减验证图方法大大提高了基于正则表达式的需求的验证性能，并实现了高效一致的早期检测。

\begin{figure}[]
  \center
  \includegraphics[width=0.7\textwidth]{allpair.pdf}
  \caption{对ToR-to-ToR可达性检查的执行时间}
  \label{fig:eval-cdf-auto-allpair}
\end{figure}

除了上述结果外，我们还展示了验证时间如何随着处理的更新数量的增加而变化。结果如图~\ref{fig:allpair-update}所示。正如我们所看到的，MT的验证时间随着更多规则更新的完成而增加，而这种趋势在DGQ方法中没有表现出来。原因是模型遍历的计算复杂度$O(|V|\times(|V|+|E|))$, 并且随着更多的规则更新完成$|E|$ 正在增加。同时，DGQ在开始时计算验证图的连通分量，其复杂性为$O(|V| + |E|)$, 以及$|E|$ 随着更多规则更新的完成而减少.

\begin{figure}[]
  \center
  \includegraphics[width=0.7\textwidth]{allpair-update.pdf}
  \caption{处理不同数量的更新后的验证时间}
  \label{fig:allpair-update}
\end{figure}

\section{本章小结}